package com.googlecode.kipler.container.dl;

import java.util.HashSet;
import java.util.Set;

import com.googlecode.kipler.common.Copyable;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.formula.ConceptDefinition;
import com.googlecode.kipler.syntax.formula.Formula;

/**
 * 
 * @author İnanç Seylan
 * 
 */
public class TBox implements FormulaBase, Copyable<TBox> {
	private GeneralTBox tg = new GeneralTBox();

	private UnfoldableTBox tu = new UnfoldableTBox();
	
	private boolean generateUnfoldable;
	
	public TBox(boolean generateUnfoldable) {
		this.generateUnfoldable = generateUnfoldable;
	}

	public void add(Formula formula) throws UnsatisfiableException {
		if (formula instanceof ConceptDefinition) {
			add((ConceptDefinition) formula);
		}
	}

	public void add(ConceptDefinition conDef) {
		if (!generateUnfoldable || !tu.add(conDef)) {
			tg.add(conDef);
		}
	}

	public boolean contains(Formula f) {
		boolean result = false;
		if (f instanceof ConceptDefinition) {
			result = contains((ConceptDefinition) f);
		}
		return result;
	}

	public boolean contains(ConceptDefinition cd) {
		return tg.contains(cd) || tu.contains(cd);
	}

	public Set<Formula> getFormulas() {
		Set<Formula> result = new HashSet<Formula>(tg.getFormulas());
		result.addAll(tu.getFormulas());
		return result;
	}

	public boolean isSatisfiable() {
		return tg.isSatisfiable() && tu.isSatisfiable();
	}

	public TBox copy() {
		TBox tbox = new TBox(generateUnfoldable);
		tbox.tg = tg.copy();
		tbox.tu = tu.copy();
		return tbox;
	}

	@Override
	public boolean equals(Object obj) {
		if (obj != null && (obj.getClass().equals(this.getClass()))) {
			TBox other = (TBox) obj;
			return this.size() == other.size() && tg.equals(other.tg)
					&& tu.equals(other.tu);
		}
		return false;
	}

	public GeneralTBox getGeneral() {
		return tg;
	}

	public UnfoldableTBox getUnfoldable() {
		return tu;
	}

	@Override
	public String toString() {
		StringBuffer buffer = new StringBuffer();
		buffer.append("TBox");
		buffer.append(" = {");
		for (Formula f : getFormulas())
			buffer.append(f + ", ");
		buffer.delete(buffer.length() - 2, buffer.length());
		buffer.append("}");
		return buffer.toString();
	}

	public int size() {
		return tg.size() + tu.size();
	}
}
